M1, M2:msga{i:l}. ma-sub{i:l}(M1; M2)  Prop{i'} 

latex

Definitions	t  T, Knd, IdLnk, x.A(x), x:A. B(x), x. t(x), 1of(t), KindDeq, Top, P  Q, IdDeq, Id, locl(a), 2of(t), rcv(l,tg), Void, Type, f(x)?z, type List, State(ds), x:AB(x), x:AB(x), #$n, a<b, False, A, AB, , {x:A| B(x) }, , Atom, Prop, a:A fp B(a), P & Q, f  g, IdLnkDeq, product-deq(A;B;a;b), A & B, Valtype(da;k), MsgA, M1  M2
Lemmas	msga wf, product-deq wf, idlnk-deq wf, fpf-sub wf, fpf-trivial-subtype-top, subtype-fpf2, subtype rel product, ma-state wf, subtype rel dep function, subtype rel self, subtype rel function, subtype rel list, fpf-cap wf, subtype-fpf-cap-void, rcv wf, pi2 wf, locl wf, Id wf, id-deq wf, subtype-fpf-cap-top, top wf, Kind-deq wf, pi1 wf, IdLnk wf, Knd wf